Section: New Results

SMT techniques for optimization problems

Participant : Germain Faure [Contact] .

The TypiCal team has collaborated with the sysmo team at the Laboratoire d'Informatique de l'École Polytechnique in order to integrate the use of automated tools like SMT solvers in the resolution of optimization problems. The case study was a problem of large scale energy management with various constraints, proposed at the ROADEF 2010 challenge won by the sysmo team. We investigated how to delegate to the SMT tool part of the resolution of constraints. A first conclusion of this experiment is that solving optimization problems represents a more important part of the computation time than first expected. As SMT solvers are not geared toward this class of problems, their performance were not satisfactory. This nonetheless opens new perspectives for the development of SMT tools in order to adapt their internal decision procedures to this new kind of benchmarks. We consider that significant progress in that direction could be easily obtained.